eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
↳ QTRS
↳ DependencyPairsProof
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
MINS(x, y, z) → IF(null(x), x, y, z)
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_RM(false, n, add(m, x)) → RM(n, x)
IF2(true, x, y, z) → APP(rm(head(x), tail(x)), y)
LE(s(x), s(y)) → LE(x, y)
IF2(false, x, y, z) → HEAD(x)
IF2(true, x, y, z) → RM(head(x), tail(x))
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
RM(n, add(m, x)) → EQ(n, m)
IF2(true, x, y, z) → MINS(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
MIN(add(n, add(m, x))) → LE(n, m)
IF(false, x, y, z) → EQ(head(x), min(x))
IF(false, x, y, z) → MIN(x)
IF2(true, x, y, z) → APP(z, add(head(x), nil))
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
APP(add(n, x), y) → APP(x, y)
MINSORT(x) → MINS(x, nil, nil)
IF2(true, x, y, z) → HEAD(x)
IF2(false, x, y, z) → TAIL(x)
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
EQ(s(x), s(y)) → EQ(x, y)
MINS(x, y, z) → NULL(x)
IF_RM(true, n, add(m, x)) → RM(n, x)
IF(false, x, y, z) → HEAD(x)
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
IF2(true, x, y, z) → TAIL(x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
MINS(x, y, z) → IF(null(x), x, y, z)
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_RM(false, n, add(m, x)) → RM(n, x)
IF2(true, x, y, z) → APP(rm(head(x), tail(x)), y)
LE(s(x), s(y)) → LE(x, y)
IF2(false, x, y, z) → HEAD(x)
IF2(true, x, y, z) → RM(head(x), tail(x))
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
RM(n, add(m, x)) → EQ(n, m)
IF2(true, x, y, z) → MINS(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
MIN(add(n, add(m, x))) → LE(n, m)
IF(false, x, y, z) → EQ(head(x), min(x))
IF(false, x, y, z) → MIN(x)
IF2(true, x, y, z) → APP(z, add(head(x), nil))
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
APP(add(n, x), y) → APP(x, y)
MINSORT(x) → MINS(x, nil, nil)
IF2(true, x, y, z) → HEAD(x)
IF2(false, x, y, z) → TAIL(x)
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
EQ(s(x), s(y)) → EQ(x, y)
MINS(x, y, z) → NULL(x)
IF_RM(true, n, add(m, x)) → RM(n, x)
IF(false, x, y, z) → HEAD(x)
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
IF2(true, x, y, z) → TAIL(x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
APP(add(n, x), y) → APP(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(add(n, x), y) → APP(x, y)
The value of delta used in the strict ordering is 1.
POL(APP(x1, x2)) = (4)x_1
POL(add(x1, x2)) = 1/4 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LE(s(x), s(y)) → LE(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LE(s(x), s(y)) → LE(x, y)
The value of delta used in the strict ordering is 1/4.
POL(s(x1)) = 1/2 + (4)x_1
POL(LE(x1, x2)) = (1/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
The value of delta used in the strict ordering is 4.
POL(add(x1, x2)) = 4 + x_2
POL(IF_MIN(x1, x2)) = (4)x_2
POL(le(x1, x2)) = 0
POL(MIN(x1)) = 4 + (4)x_1
POL(true) = 0
POL(false) = 0
POL(s(x1)) = 0
POL(0) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
EQ(s(x), s(y)) → EQ(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
EQ(s(x), s(y)) → EQ(x, y)
The value of delta used in the strict ordering is 1.
POL(EQ(x1, x2)) = x_2
POL(s(x1)) = 1 + x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)
The value of delta used in the strict ordering is 4.
POL(RM(x1, x2)) = (4)x_2
POL(add(x1, x2)) = 2 + (2)x_2
POL(eq(x1, x2)) = 0
POL(IF_RM(x1, x2, x3)) = (2)x_3
POL(true) = 0
POL(false) = 0
POL(s(x1)) = 0
POL(0) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
MINS(x, y, z) → IF(null(x), x, y, z)
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
IF2(true, x, y, z) → MINS(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)